InforLorV4, Main, Exploration, bibRecord, 005604

Formal and incremental construction of distributed algorithms : On the distributed reference counting algorithm

Identifieur interne : 005604 ( Main/Exploration ); précédent : 005603; suivant : 005605

Formal and incremental construction of distributed algorithms : On the distributed reference counting algorithm

Auteurs : Dominique Cansell [France] ; Dominique Méry [France]

Source :

Theoretical computer science [ 0304-3975 ] ; 2006.

RBID : Pascal:06-0539921

Descripteurs français

Pascal (Inist)
- Algorithme réparti, Système réparti, Système complexe, Spécification, Vérification, Informatique théorique, Modélisation, Affinement, Abstraction, Preuve, Problème comptage, Aide preuve.
Wicri :
- topic : Preuve.

English descriptors

KwdEn :
- Abstraction, Complex system, Computer theory, Distributed algorithm, Distributed system, Modeling, Proof assistant, Refinement, Specification, Verification.
mix :
- abstraction, distributed algorithms, modeling, proof, proof assistant, refinement, specification, verification.

Abstract

The development of distributed algorithms and, more generally, distributed systems, is a complex, delicate and challenging process. Refinement techniques of (system) models improve the process by using a proof assistant, and by applying a design methodology aimed at starting from the most abstract model and leading, in an incremental way, to the most concrete model, for producing a distributed solution. We show, using the distributed reference counting (DRC) problem as our study, how models can be produced in an elegant and progressive way, thanks to the refinement and how the final distributed algorithm is built starting from these models. The development is carried out within the framework of the event B method and models are validated with a proof assistant.

Url:

https://hal.inria.fr/inria-00093164

Affiliations:

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Formal and incremental construction of distributed algorithms : On the distributed reference counting algorithm</title>
<author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
<affiliation wicri:level="4"><inist:fA14 i1="01"><s1>Université de Metz</s1>
<s2>57045 Metz</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Metz</settlement>
</placeName>
<orgName type="university">Université Paul Verlaine - Metz</orgName>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
<author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Mery">Dominique Méry</name>
<affiliation wicri:level="4"><inist:fA14 i1="02"><s1>Université Henri Poincaré, LORIA, BP239</s1>
<s2>54506 Vandoeuvre-lès Nancy</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
<orgName type="university">Université Henri Poincaré</orgName>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">06-0539921</idno>
<date when="2006">2006</date>
<idno type="stanalyst">PASCAL 06-0539921 INIST</idno>
<idno type="RBID">Pascal:06-0539921</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000411</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000622</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000383</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000383</idno>
<idno type="wicri:doubleKey">0304-3975:2006:Cansell D:formal:and:incremental</idno>
<idno type="wicri:Area/Main/Merge">005788</idno>
<idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:inria-00093164</idno>
<idno type="url">https://hal.inria.fr/inria-00093164</idno>
<idno type="wicri:Area/Hal/Corpus">002394</idno>
<idno type="wicri:Area/Hal/Curation">002394</idno>
<idno type="wicri:Area/Hal/Checkpoint">004359</idno>
<idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">004359</idno>
<idno type="wicri:doubleKey">0304-3975:2006:Cansell D:formal:and:incremental</idno>
<idno type="wicri:Area/Main/Merge">005998</idno>
<idno type="wicri:Area/Main/Curation">005604</idno>
<idno type="wicri:Area/Main/Exploration">005604</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Formal and incremental construction of distributed algorithms : On the distributed reference counting algorithm</title>
<author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
<affiliation wicri:level="4"><inist:fA14 i1="01"><s1>Université de Metz</s1>
<s2>57045 Metz</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Metz</settlement>
</placeName>
<orgName type="university">Université Paul Verlaine - Metz</orgName>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
<author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Mery">Dominique Méry</name>
<affiliation wicri:level="4"><inist:fA14 i1="02"><s1>Université Henri Poincaré, LORIA, BP239</s1>
<s2>54506 Vandoeuvre-lès Nancy</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
<orgName type="university">Université Henri Poincaré</orgName>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Theoretical computer science</title>
<title level="j" type="abbreviated">Theor. comput. sci.</title>
<idno type="ISSN">0304-3975</idno>
<imprint><date when="2006">2006</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Theoretical computer science</title>
<title level="j" type="abbreviated">Theor. comput. sci.</title>
<idno type="ISSN">0304-3975</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Abstraction</term>
<term>Complex system</term>
<term>Computer theory</term>
<term>Distributed algorithm</term>
<term>Distributed system</term>
<term>Modeling</term>
<term>Proof assistant</term>
<term>Refinement</term>
<term>Specification</term>
<term>Verification</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Algorithme réparti</term>
<term>Système réparti</term>
<term>Système complexe</term>
<term>Spécification</term>
<term>Vérification</term>
<term>Informatique théorique</term>
<term>Modélisation</term>
<term>Affinement</term>
<term>Abstraction</term>
<term>Preuve</term>
<term>Problème comptage</term>
<term>Aide preuve</term>
</keywords>
<keywords scheme="Wicri" type="topic" xml:lang="fr"><term>Preuve</term>
</keywords>
<keywords scheme="mix" xml:lang="en"><term>abstraction</term>
<term>distributed algorithms</term>
<term>modeling</term>
<term>proof</term>
<term>proof assistant</term>
<term>refinement</term>
<term>specification</term>
<term>verification</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">The development of distributed algorithms and, more generally, distributed systems, is a complex, delicate and challenging process. Refinement techniques of (system) models improve the process by using a proof assistant, and by applying a design methodology aimed at starting from the most abstract model and leading, in an incremental way, to the most concrete model, for producing a distributed solution. We show, using the distributed reference counting (DRC) problem as our study, how models can be produced in an elegant and progressive way, thanks to the refinement and how the final distributed algorithm is built starting from these models. The development is carried out within the framework of the event B method and models are validated with a proof assistant.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
</country>
<region><li>Grand Est</li>
<li>Lorraine (région)</li>
</region>
<settlement><li>Metz</li>
<li>Nancy</li>
<li>Vandœuvre-lès-Nancy</li>
</settlement>
<orgName><li>Centre national de la recherche scientifique</li>
<li>Institut national de recherche en informatique et en automatique</li>
<li>Laboratoire lorrain de recherche en informatique et ses applications</li>
<li>Mosel (Loria)</li>
<li>Université Henri Poincaré</li>
<li>Université Paul Verlaine - Metz</li>
<li>Université de Lorraine</li>
</orgName>
</list>
<tree><country name="France"><region name="Grand Est"><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
</region>
<name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Mery">Dominique Méry</name>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 005604 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 005604 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     Pascal:06-0539921
   |texte=   Formal and incremental construction of distributed algorithms : On the distributed reference counting algorithm
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

Serveur d'exploration sur la recherche en informatique en Lorraine

Formal and incremental construction of distributed algorithms : On the distributed reference counting algorithm

Formal and incremental construction of distributed algorithms : On the distributed reference counting algorithm

Source :

Descripteurs français

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.